Skip to content

feat(NumberTheory): add Sylvester-Schur theorem#39251

Closed
akiezun wants to merge 2 commits into
leanprover-community:masterfrom
akiezun:feat/sylvester-schur
Closed

feat(NumberTheory): add Sylvester-Schur theorem#39251
akiezun wants to merge 2 commits into
leanprover-community:masterfrom
akiezun:feat/sylvester-schur

Conversation

@akiezun
Copy link
Copy Markdown

@akiezun akiezun commented May 12, 2026 •
edited
Loading

This PR formalizes the Sylvester-Schur theorem.

The main new theorem is: Nat.exists_prime_gt_and_dvd_ascFactorial

It states that if 0 < k and k < n, then some prime p > k divides n.ascFactorial k.

The proof follows Erdős's proof of Sylvester-Schur, cited in the module docstring and added to docs/references.bib.

The implementation is in Mathlib/NumberTheory/SylvesterSchur/, with a top-level re-export file at Mathlib/NumberTheory/SylvesterSchur.lean. Most proof infrastructure is private or kept inside the Sylvester-Schur
namespace/files.

I used AI assistance (Codex 5.5) while developing this formalization. I have reviewed the submitted code.

Open in Gitpod

@github-actions github-actions Bot added the new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! label May 12, 2026
@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 12, 2026

Welcome new contributor!

Thank you for contributing to Mathlib! If you haven't done so already, please review our contribution guidelines, as well as the style guide and naming conventions. In particular, we kindly remind contributors that we have guidelines regarding the use of AI when making pull requests.

We use a review queue to manage reviews. If your PR does not appear there, it is probably because it is not successfully building (i.e., it doesn't have a green checkmark), has the awaiting-author tag, or another reason described in the Lifecycle of a PR. The review dashboard has a dedicated webpage which shows whether your PR is on the review queue, and (if not), why.

If you haven't already done so, please come to https://leanprover.zulipchat.com/, introduce yourself, and mention your new PR.

Thank you again for joining our community.

@akiezun akiezun changed the title Feat/sylvester schur feat(NumberTheory): add Sylvester-Schur theorem May 12, 2026
@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 12, 2026

PR summary 686c76b39d

Import changes for modified files

No significant changes to the import graph

Import changes for all files
Files Import difference
Mathlib.NumberTheory.SylvesterSchur.ResidualLarge.PowerBounds (new file) 620
Mathlib.NumberTheory.SylvesterSchur.ResidualLarge.ScaledTernaryBound (new file) 628
Mathlib.NumberTheory.SylvesterSchur.Bridge (new file) 760
Mathlib.NumberTheory.SylvesterSchur.PrimeCounting (new file) 1075
Mathlib.NumberTheory.SylvesterSchur.ResidualLarge.TinyPrimeCountingBound (new file) 1096
Mathlib.NumberTheory.SylvesterSchur.ChooseFactorization (new file) 1144
Mathlib.NumberTheory.SylvesterSchur.ErdosLayers (new file) 1146
Mathlib.NumberTheory.SylvesterSchur.ErdosPowerBounds (new file) 1147
Mathlib.NumberTheory.SylvesterSchur.LargePrimeCriteria (new file) 1148
Mathlib.NumberTheory.SylvesterSchur.ResidualLarge.CentralOffsetBound (new file) 1150
Mathlib.NumberTheory.SylvesterSchur.ResidualLarge (new file) 1152
Mathlib.NumberTheory.SylvesterSchur.Conditional (new file) 2037
Mathlib.NumberTheory.SylvesterSchur.BlockReductions (new file) 2039
Mathlib.NumberTheory.SylvesterSchur.ResidualFinite (new file) 2040
Mathlib.NumberTheory.SylvesterSchur.ResidualLargeCertificates (new file) 2041
Mathlib.NumberTheory.SylvesterSchur.ErdosKey (new file) 2047
Mathlib.NumberTheory.SylvesterSchur.Main (new file) 2048
Mathlib.NumberTheory.SylvesterSchur (new file) 2049

Declarations diff

+ base_two_pow_exp
+ bertrand_base
+ binomial_iff_consecutive
+ binomial_of_consecutive
+ binomial_sylvester_schur
+ block_length_le_smoothNumbersUpTo_bound_of_no_large_prime_dvd_block
+ block_length_le_smoothNumbersUpTo_card_of_no_large_prime_dvd_block
+ block_term_mem_smoothNumbers_succ_of_no_large_prime_dvd_block
+ block_term_prime_factors_le_of_no_large_prime_dvd_block
+ cancelled_bound_of_base_pow_exponent_cap
+ cancelled_bound_of_base_pow_exponent_cap_le
+ card_finsetUnionList_le_cardSum
+ central_erdos_layers_two_mul_add_two_lt_four_pow
+ central_layers_le_four_pow_of_lt_three_mul
+ central_layers_two_mul_add_two_le_four_pow
+ central_offset_div_three_choose
+ choose_eq_prod_prime_factorization_layers
+ choose_eq_prod_small_prime_powers_of_no_large
+ choose_factorization_pow_le_self_of_sqrt_lt
+ choose_large_factorization_product_le_primorial
+ choose_le_prod_erdos_central_layers_of_no_large
+ choose_le_prod_erdos_div_three_layers_of_no_large
+ choose_le_prod_erdos_layers_of_no_large
+ choose_le_prod_primorial_nthRoot_of_no_large
+ choose_le_top_pow_half_add_one_of_no_large
+ choose_le_top_pow_primeCounting_of_no_large
+ choose_le_top_pow_sqrt_mul_primorial_of_no_large
+ choose_le_top_pow_sub_one_of_no_large
+ choose_le_top_pow_succ_of_no_large
+ choose_le_top_pow_three_mul_div_eight_of_no_large
+ choose_small_factorization_product_le_top_pow_sqrt
+ consecutive_base_start
+ consecutive_five
+ consecutive_five_finite_certificate
+ consecutive_five_witness
+ consecutive_five_witness_mod_fifteen_to_twenty_nine
+ consecutive_five_witness_mod_forty_five_to_fifty_nine
+ consecutive_five_witness_mod_lt_fifteen
+ consecutive_five_witness_mod_thirty_to_forty_four
+ consecutive_four
+ consecutive_of_binomial
+ consecutive_of_exists_prime_dvd_choose
+ consecutive_of_factorial_mul_prod_erdos_central_layers_lt_start_pow
+ consecutive_of_factorial_mul_prod_erdos_div_three_layers_lt_start_pow
+ consecutive_of_factorial_mul_prod_erdos_layers_lt_start_pow
+ consecutive_of_factorial_mul_prod_primorial_nthRoot_lt_start_pow
+ consecutive_of_factorial_mul_top_pow_half_add_one_lt_start_pow
+ consecutive_of_factorial_mul_top_pow_primeCounting_lt_start_pow
+ consecutive_of_factorial_mul_top_pow_sqrt_mul_primorial_lt_start_pow
+ consecutive_of_factorial_mul_top_pow_sub_one_lt_start_pow
+ consecutive_of_factorial_mul_top_pow_three_mul_div_eight_lt_start_pow
+ consecutive_of_large_start
+ consecutive_of_mul_prod_erdos_central_layers_lt_four_pow
+ consecutive_of_mul_top_pow_sqrt_mul_primorial_lt_four_pow
+ consecutive_of_quadratic_start
+ consecutive_of_self_pow_mul_top_pow_three_mul_div_eight_lt_start_pow
+ consecutive_of_three_eighth_large_start
+ consecutive_of_three_eighth_self_pow_large_start
+ consecutive_one
+ consecutive_six
+ consecutive_sylvester_schur
+ consecutive_three
+ consecutive_three_witness
+ consecutive_two
+ const_log_product_le_one_fifth_of_le_four_mul
+ const_log_product_le_three_halves
+ const_log_product_le_two_thirds_of_le_sixty_four_mul
+ cube_le_two_pow_of_ten_le
+ cube_succ_le_two_pow_three_mul_div_four_add_one
+ erdos_choose_prime_factor_gt
+ erdos_choose_prime_factor_gt_base_start
+ erdos_choose_prime_factor_gt_bertrand_steps
+ erdos_choose_prime_factor_gt_bound_dispatch_core
+ erdos_choose_prime_factor_gt_bound_dispatch_tail
+ erdos_choose_prime_factor_gt_hard
+ erdos_choose_prime_factor_gt_length_one
+ erdos_choose_prime_factor_gt_of_bertrand_overshoot
+ erdos_choose_prime_factor_gt_second_residual
+ erdos_choose_prime_factor_gt_second_residual_finite
+ erdos_choose_prime_factor_gt_second_residual_large
+ erdos_choose_prime_factor_gt_second_start
+ erdos_choose_prime_factor_gt_small_length
+ erdos_div_three_layers_le_four_pow
+ erdos_layers_le_four_pow
+ erdos_layers_le_four_pow_aux
+ erdos_layers_le_four_pow_three_layers
+ erdos_layers_le_four_pow_three_layers_aux
+ erdos_layers_le_four_pow_three_layers_of_zero_mem_not_one_mem
+ erdos_layers_le_four_pow_three_layers_of_zero_not_mem
+ erdos_layers_le_four_pow_three_layers_of_zero_one_mem
+ erdos_layers_tail_le_four_pow_cuberoot
+ erdos_layers_tail_le_four_pow_of_nthRoot_le
+ erdos_layers_tail_le_four_pow_sqrt
+ exists_dvd_block_of_succ_succ_prime_not_dvd_pred
+ exists_dvd_block_or_dvd_recent_pred
+ exists_dvd_consecutive_of_prime_dvd_choose
+ exists_large_prime_dvd_central_choose
+ exists_large_prime_dvd_choose_of_factorial_mul_prod_erdos_central_layers_lt_lower_pow
+ exists_large_prime_dvd_choose_of_factorial_mul_prod_erdos_div_three_layers_lt_lower_pow
+ exists_large_prime_dvd_choose_of_factorial_mul_prod_erdos_layers_lt_lower_pow
+ exists_large_prime_dvd_choose_of_factorial_mul_prod_primorial_nthRoot_lt_lower_pow
+ exists_large_prime_dvd_choose_of_factorial_mul_top_pow_half_add_one_lt_lower_pow
+ exists_large_prime_dvd_choose_of_factorial_mul_top_pow_primeCounting_lt_lower_pow
+ exists_large_prime_dvd_choose_of_factorial_mul_top_pow_sqrt_mul_primorial_lt_lower_pow
+ exists_large_prime_dvd_choose_of_factorial_mul_top_pow_sub_one_lt_lower_pow
+ exists_large_prime_dvd_choose_of_factorial_mul_top_pow_three_mul_div_eight_lt_lower_pow
+ exists_large_prime_dvd_choose_of_mul_prod_erdos_central_layers_lt_four_pow
+ exists_large_prime_dvd_choose_of_mul_top_pow_sqrt_mul_primorial_lt_four_pow
+ exists_large_prime_dvd_choose_of_not_forall_prime_dvd_le
+ exists_large_prime_dvd_choose_of_prod_erdos_central_layers_lt_choose
+ exists_large_prime_dvd_choose_of_prod_erdos_central_layers_lt_lower_bound
+ exists_large_prime_dvd_choose_of_prod_erdos_div_three_layers_lt_choose
+ exists_large_prime_dvd_choose_of_prod_erdos_div_three_layers_lt_lower_bound
+ exists_large_prime_dvd_choose_of_prod_erdos_layers_lt_choose
+ exists_large_prime_dvd_choose_of_prod_erdos_layers_lt_lower_bound
+ exists_large_prime_dvd_choose_of_prod_primorial_nthRoot_lt_choose
+ exists_large_prime_dvd_choose_of_prod_primorial_nthRoot_lt_lower_bound
+ exists_large_prime_dvd_choose_of_self_pow_mul_top_pow_three_mul_div_eight_lt_lower_pow
+ exists_large_prime_dvd_choose_of_top_pow_half_add_one_lt_choose
+ exists_large_prime_dvd_choose_of_top_pow_half_add_one_lt_lower_bound
+ exists_large_prime_dvd_choose_of_top_pow_primeCounting_lt_choose
+ exists_large_prime_dvd_choose_of_top_pow_primeCounting_lt_lower_bound
+ exists_large_prime_dvd_choose_of_top_pow_sqrt_mul_primorial_lt_choose
+ exists_large_prime_dvd_choose_of_top_pow_sqrt_mul_primorial_lt_lower_bound
+ exists_large_prime_dvd_choose_of_top_pow_sub_one_lt_choose
+ exists_large_prime_dvd_choose_of_top_pow_sub_one_lt_lower_bound
+ exists_large_prime_dvd_choose_of_top_pow_three_mul_div_eight_lt_choose
+ exists_large_prime_dvd_choose_of_top_pow_three_mul_div_eight_lt_lower_bound
+ exists_large_prime_dvd_choose_of_upper_lt_lower
+ exists_large_prime_factor_in_block_of_prime_near
+ exists_prime_dvd_choose_of_block_interval
+ exists_prime_dvd_choose_of_central_offset_erdos_div_three_layers_bound
+ exists_prime_dvd_choose_of_erdos_div_three_layers_bound
+ exists_prime_dvd_choose_of_erdos_layers_bound
+ exists_prime_dvd_choose_of_erdos_layers_four_pow_bound
+ exists_prime_dvd_choose_of_erdos_layers_three_layers_bound
+ exists_prime_dvd_choose_of_half_bound
+ exists_prime_dvd_choose_of_large_prime_dvd_block
+ exists_prime_dvd_choose_of_large_prime_dvd_term
+ exists_prime_dvd_choose_of_large_start
+ exists_prime_dvd_choose_of_primeCounting_bound
+ exists_prime_dvd_choose_of_scaled_ternary_erdos_layers_bound
+ exists_prime_dvd_choose_of_smooth_count_bound
+ exists_prime_dvd_choose_of_sqrt_primorial_bound
+ exists_prime_dvd_choose_two_mul_add_two_small
+ exists_prime_gt_and_dvd_ascFactorial
+ exists_prime_gt_five_dvd_of_not_two_dvd_of_not_three_dvd_of_not_five_dvd
+ exists_prime_gt_three_dvd_of_not_two_dvd_of_not_three_dvd
+ exists_prime_near_mid_range_high
+ exists_prime_near_mid_range_high_low
+ exists_prime_near_mid_range_high_top
+ exists_prime_near_mid_range_low
+ exists_prime_near_mid_range_middle
+ exists_prime_near_mid_range_top
+ exists_prime_near_of_ge_forty_one_lt_1291
+ exists_prime_near_seven_of_ge_ten_lt_100
+ exists_prime_near_six_high
+ exists_prime_near_six_low
+ exists_prime_near_six_of_ge_ten_lt_100_ne_ninety
+ factorialSieveCandidates
+ factorialSieveCandidates_card_le_509
+ factorialSieveCandidates_card_le_715
+ factorialSieveCandidates_card_le_855
+ factorialSieveCandidates_card_le_917
+ factorialSieveCandidates_card_le_940
+ factorialSieveCandidates_card_le_944
+ factorialSieveCandidates_card_le_of_chunks
+ factorialSieveCandidates_subset_sieveChunks509
+ factorialSieveCandidates_subset_sieveChunks715
+ factorialSieveCandidates_subset_sieveChunks855
+ factorialSieveCandidates_subset_sieveChunks917
+ factorialSieveCandidates_subset_sieveChunks940
+ factorialSieveCandidates_subset_sieveChunks944
+ factorialSieveCandidates_subset_sieveChunksOfBounds
+ factorial_mul_scaled_primeCounting_lt_of_segment
+ factorial_mul_top_pow_sub_one_lt_start_pow_of_large_start
+ factorial_scaled_bound_of_le
+ factorial_scaled_bound_step
+ finsetCardSum
+ finsetUnionList
+ first_layer_central_prime_product_le_primorial_div_three
+ first_layer_prime_product_le_primorial
+ first_layer_prime_product_le_primorial_div_three
+ first_layer_prime_product_le_primorial_div_three_aux
+ first_residual_large_cancelled_bound
+ first_residual_large_cancelled_bound_range_16_64
+ first_residual_large_cancelled_bound_range_3_4
+ first_residual_large_cancelled_bound_range_4_8
+ first_residual_large_cancelled_bound_range_512
+ first_residual_large_cancelled_bound_range_64_512
+ first_residual_large_cancelled_bound_range_8_16
+ first_residual_large_exponent_le_four_fifteenths
+ first_residual_large_exponent_le_nine_fourths
+ first_residual_large_exponent_le_self
+ first_residual_large_exponent_le_three_fourths
+ first_residual_large_exponent_le_three_mul_self
+ first_residual_large_exponent_le_two_fifths
+ first_residual_large_root_log_le_three_fifths_of_le_sixteen_mul
+ first_residual_large_root_log_le_three_halves_of_le_five_twelve_mul
+ first_residual_large_root_log_le_three_tenths_of_le_eight_mul
+ first_residual_large_root_log_le_two_mul_self
+ first_residual_large_root_log_le_two_thirds_of_le_sixty_four_mul
+ first_residual_large_scaled_ternary_bound
+ four_lt_of_prime_of_three_lt
+ four_pow_mul_two_pow_mul_four_pow_lt_three_pow_mul_four_pow
+ half_witness_five
+ half_witness_three
+ layer_prime_product_le_primorial_nthRoot
+ layer_prime_product_lt_factorization_le_primorial_nthRoot
+ log_two_le_three_mul_nthRoot_three_div_four
+ log_two_le_two_mul_sqrt_nthRoot_three
+ log_two_two_mul_add_two_le_nthRoot_three
+ mem_finsetUnionList_sieveChunksOfBounds
+ mul_three_mul_div_four_le_mul_div_of_scaled_sq
+ mul_top_pow_lt_start_pow_of_scaled_top_le_start
+ mul_top_pow_lt_start_pow_of_two_mul_top_le_three_mul_start
+ nthRoot_le_nthRoot_three_of_three_le
+ nthRoot_le_sqrt_of_two_le
+ nthRoot_three_mul_log_le_mul_div_of_scaled_sq
+ nthRoot_three_mul_log_le_mul_pred_of_nthRoot_lt
+ nthRoot_three_mul_log_le_of_nthRoot_lt
+ nthRoot_three_mul_log_le_one_fifth_of_ge_sixteen
+ nthRoot_three_mul_log_le_one_fifth_of_le_four_mul
+ nthRoot_three_mul_log_le_one_fifth_of_lt
+ nthRoot_three_mul_log_le_one_fifth_of_nthRoot_ge
+ nthRoot_three_mul_log_le_three_halves_of_ge_seventy_nine
+ nthRoot_three_mul_log_le_three_halves_of_lt
+ nthRoot_three_mul_log_le_three_halves_of_lt_eighty_one
+ nthRoot_three_mul_log_le_three_halves_of_sq_le
+ nthRoot_three_mul_log_le_two_thirds_of_lt
+ nthRoot_three_mul_log_le_two_thirds_of_nthRoot_ge
+ nthRoot_three_pow_le_of_le
+ nthRoot_three_sq_le_two_mul_of_ge_two_fifty_six
+ nthRoot_three_two_mul_add_two_sq_le_div_four
+ nthRoot_two_le_sqrt
+ pow1291_1
+ pow1291_128
+ pow1291_128_eq
+ pow1291_16
+ pow1291_16_eq
+ pow1291_17_eq
+ pow1291_1_eq
+ pow1291_2
+ pow1291_213_eq
+ pow1291_256
+ pow1291_256_eq
+ pow1291_2_eq
+ pow1291_32
+ pow1291_32_eq
+ pow1291_383_eq
+ pow1291_39_eq
+ pow1291_4
+ pow1291_4_eq
+ pow1291_512
+ pow1291_512_eq
+ pow1291_569_eq
+ pow1291_64
+ pow1291_64_eq
+ pow1291_700_eq
+ pow1291_759_eq
+ pow1291_781_eq
+ pow1291_8
+ pow1291_8_eq
+ pow1291_95_eq
+ pow_mul_choose_le_pow_mul_choose
+ pow_mul_descFactorial_le_pow_mul_descFactorial
+ pow_six_step_of_ten_le
+ primeCounting_le_157
+ primeCounting_le_309
+ primeCounting_le_509
+ primeCounting_le_715
+ primeCounting_le_75
+ primeCounting_le_855
+ primeCounting_le_917
+ primeCounting_le_940
+ primeCounting_le_944
+ primeCounting_le_half_add_one
+ primeCounting_le_mod_thirty
+ primeCounting_le_of_factorial_sieve_card
+ primeCounting_le_self
+ primeCounting_le_small_sieve
+ primeCounting_le_sub_one
+ primeCounting_le_three_mul_div_eight
+ prime_coprime_smallSieveProduct_of_twenty_nine_lt
+ prime_dvd_choose_of_dvd_consecutive
+ prime_dvd_choose_of_mem_interval
+ prime_dvd_seq_implies_choose
+ prime_mem_smallSievePrimes_of_le_twenty_nine
+ prod_range_ite_lt_eq_pow
+ range_16_base_exp
+ range_3_base_exp
+ range_4_base_exp
+ range_512_base_exp
+ range_64_base_exp
+ range_8_base_exp
+ scaled_pow_le_of_le
+ scaled_ternary_bound_of_cancelled
+ scaled_ternary_choose
+ second_residual_large_central_offset_bound
+ second_residual_mid_base_158
+ second_residual_mid_base_310
+ second_residual_mid_base_38
+ second_residual_mid_base_510
+ second_residual_mid_base_716
+ second_residual_mid_base_76
+ second_residual_mid_base_856
+ second_residual_mid_base_918
+ second_residual_mid_base_941
+ second_residual_mid_has_large_prime_factor
+ second_residual_mid_primeCounting_lt_start_pow
+ second_residual_tiny_has_large_prime_factor
+ second_residual_tiny_primeCounting_lt_start_pow
+ self_le_two_pow_two_mul_div_one_twenty_eight_add_one
+ sieveBounds509
+ sieveBounds715
+ sieveBounds855
+ sieveBounds917
+ sieveBounds940
+ sieveBounds944
+ sieveChunk
+ sieveChunk_card_le_0_99
+ sieveChunk_card_le_100_199
+ sieveChunk_card_le_200_299
+ sieveChunk_card_le_300_399
+ sieveChunk_card_le_400_499
+ sieveChunk_card_le_500_509
+ sieveChunk_card_le_500_599
+ sieveChunk_card_le_600_699
+ sieveChunk_card_le_700_715
+ sieveChunk_card_le_700_799
+ sieveChunk_card_le_800_855
+ sieveChunk_card_le_800_899
+ sieveChunk_card_le_900_917
+ sieveChunk_card_le_900_940
+ sieveChunk_card_le_900_944
+ sieveChunks509
+ sieveChunks715
+ sieveChunks855
+ sieveChunks917
+ sieveChunks940
+ sieveChunks944
+ sieveChunksOfBounds
+ six_lt_of_prime_of_five_lt
+ smallSievePrimes
+ smallSieveProduct
+ sqrt_le_div_fifteen_of_le_four_mul
+ sqrt_le_div_of_sq_mul_le
+ sqrt_le_div_seven_of_le_sixteen_mul
+ sqrt_le_div_ten_of_le_eight_mul
+ sqrt_le_div_three_of_le_sixty_four_mul
+ sqrt_le_self_of_le_sq_add_self
+ sqrt_le_three_mul_div_four_of_le_five_twelve_mul
+ sqrt_succ_pow_six_le_two_pow_two_mul_add_one
+ sqrt_two_mul_add_two_le_div_fifteen
+ start_le_quadratic_of_no_large_prime_dvd_block
+ sylvester_schur_core
+ three_mul_choose_two_mul_add_le_two_mul_choose_succ
+ three_pow_mul_centralBinom_le_two_pow_mul_choose_three_mul
+ three_pow_mul_centralBinom_le_two_pow_mul_choose_two_mul_add
+ three_pow_mul_four_pow_lt_mul_two_pow_mul_choose_three_mul
+ two_pow_mul_four_pow_div_four_le_three_pow
+ two_pow_nineteen_mul_div_twelve_le_three_pow
++ four_pow_eq_two_pow_two_mul
++ self_le_four_pow_div_one_twenty_eight_add_one

You can run this locally as follows 
## from your `mathlib4` directory:
git clone https://github.com/leanprover-community/mathlib-ci.git ../mathlib-ci

## summary with just the declaration names:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh <optional_commit>

## more verbose report:
../mathlib-ci/scripts/pr_summary/declarations_diff.sh long <optional_commit>

The doc-module for scripts/pr_summary/declarations_diff.sh in the mathlib-ci repository contains some details about this script.

No changes to strong technical debt.
No changes to weak technical debt.

@github-actions github-actions Bot added the t-number-theory Number theory (also use t-algebra or t-analysis to specialize) label May 12, 2026
@github-actions
Copy link
Copy Markdown

github-actions Bot commented May 12, 2026 •
edited
Loading

✅ PR Title Formatted Correctly

The title of this PR has been updated to match our commit style conventions.
Thank you!

@wwylele
Copy link
Copy Markdown
Collaborator

wwylele commented May 12, 2026

I suspect it is hard for reviewers to review 5k lines of code at once. Could you split this into small PRs, starting with common lemmas that can be most likely reused by other theorems?

@akiezun
Copy link
Copy Markdown
Author

akiezun commented May 12, 2026

I suspect it is hard for reviewers to review 5k lines of code at once. Could you split this into small PRs, starting with common lemmas that can be most likely reused by other theorems?

Possibly. Some candidates below. What do you think?

  • primeCounting_le_sub_one: There are at most r - 1 primes less than or equal to r, for 2 ≤ r.

  • primeCounting_le_half_add_one: There are at most r / 2 + 1 primes less than or equal to r.

  • primeCounting_le_three_mul_div_eight: For 38 ≤ r, there are at most 3r / 8 primes less than or equal to r.

  • exists_large_prime_dvd_choose_of_not_forall_prime_dvd_le: If not every prime divisor of Nat.choose N r is at most r, then Nat.choose N r has a prime divisor greater than r.

  • exists_large_prime_dvd_choose_of_upper_lt_lower: If assuming all prime divisors of Nat.choose N r are at most r gives an upper bound below Mathlib’s lower bound for Nat.choose N r, then some prime divisor is greater
    than r.

  • choose_eq_prod_small_prime_powers_of_no_large: If every prime divisor of Nat.choose N r is at most r, then the prime factorization product for Nat.choose N r can be truncated to primes up to r.

  • choose_le_top_pow_primeCounting_of_no_large: If every prime divisor of Nat.choose N r is at most r, then Nat.choose N r ≤ N ^ Nat.primeCounting r.

  • choose_le_top_pow_sub_one_of_no_large: Under the same no-large-prime hypothesis, Nat.choose N r ≤ N ^ (r - 1).

  • choose_le_top_pow_half_add_one_of_no_large: Under the same no-large-prime hypothesis, Nat.choose N r ≤ N ^ (r / 2 + 1).

  • choose_le_top_pow_three_mul_div_eight_of_no_large: For 38 ≤ r, under the no-large-prime hypothesis, Nat.choose N r ≤ N ^ (3r / 8).

  • prime_dvd_choose_of_dvd_consecutive: If a prime p > n divides one term of the block k, ..., k+n-1, then p divides Nat.choose (k+n-1) n.

  • exists_dvd_consecutive_of_prime_dvd_choose: If a prime p > n divides Nat.choose (k+n-1) n, then p divides some term of the block k, ..., k+n-1.

  • consecutive_of_exists_prime_dvd_choose: A large prime divisor of the corresponding binomial coefficient gives a large prime divisor in the consecutive block.

  • pow_mul_choose_le_pow_mul_choose: For r ≤ M ≤ N, the scaled binomial inequality N^r * Nat.choose M r ≤ M^r * Nat.choose N r holds.

@mathlib-triage
Copy link
Copy Markdown

mathlib-triage Bot commented May 12, 2026

We appreciate your desire to contribute to mathlib. Unfortunately, this PR does not meet community standards.

Our reviewer time is very limited so we must prioritize both individuals who can learn and contribute back to the community and sufficiently high quality content as to make the process smooth and valuable.

@mathlib-triage mathlib-triage Bot added the LLM-generated PRs with substantial input from LLMs - review accordingly label May 12, 2026
@mathlib-triage mathlib-triage Bot closed this May 12, 2026
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

LLM-generated PRs with substantial input from LLMs - review accordingly new-contributor This PR was made by a contributor with at most 5 merged PRs. Welcome to the community! t-number-theory Number theory (also use t-algebra or t-analysis to specialize)

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@akiezun @wwylele